($e$.$P$($e$) $\rightarrow\rightarrow$ ${\it e'}$.$Q$(${\it e'}$)) with $R$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$$f$:\{$e$:E$\mid$ $P$($e$)\} $\rightarrow$\{$e$:E$\mid$ $Q$($e$)\} . ($e$.$P$($e$) $\rightarrow$$a$.$f$($a$)$\rightarrow$ ${\it e'}$.$Q$(${\it e'}$)) with $R$